<?php
highlight_file(__FILE__);
mt_srand(372619038);
$a = intval(mt_rand());
echo $a; // 1155388967
?>